Nuprl Definition : w-V
0,22
postcript
pdf
V(
i
;
k
) == kindcase(
k
;
a
.1of(2of(
w
))(
i
,
a
);
l
,
tg
.1of(2of(2of(
w
)))(
l
,
tg
) )
latex
clarification:
w-V(
w
;
i
;
k
) == kindcase(
k
;
a
.1of(2of(
w
))(
i
,
a
);
l
,
tg
.1of(2of(2of(
w
)))(
l
,
tg
) )
latex
Definitions
2of(
t
)
,
1of(
t
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
FDL editor aliases
w-V
origin